Inference at * 1 1 0 
Iof proof for Lemma l before transitivity:



1. T : Type
2. l : T List
3. x : T
4. y : T
5. z : T
6. no_repeats(T;l)
7. [x; y]  l
8. [y; z]  l
  [x; z]  [x; y; z] 

latex

 by PERMUTE{1:n, 2:n, 2:n, 3:n, 4:n, 5:n} 

latex

 1: .....wf..... NILNIL

 1:   T  Type
 2: .....wf..... NILNIL

 2:   x  T
 3: .....wf..... NILNIL

 3:   [z]  (T List)
 4: .....wf..... NILNIL

 4:   [y; z]  (T List)
 5: 

 5:   (x = x & [z]  [y; z])  [x; z]  [y; z]
 .

Definitions	t  T, x:A  B(x), f(a), x:AB(x), s = t, P  Q, [], [car / cdr], L1  L2, no_repeats(T;l), type List, Type, P  Q, x:A. B(x), P  Q, P & Q, P  Q
Lemmas	cons sublist cons